es:event_system{i:l}, ds:fpf(Id; x.Type), da:fpf(Knd; k.Type), i:Id.
(x:Id. subtype_rel(es-vartype(es; i; x); fpf-cap(ds; id-deq; x; top)))
 (e:es-E(es). 
 (loc(e) = i)  subtype_rel(es-valtype(es; e); fpf-cap(da; Kind-deq; es-kind(es; e); top)))
 (e:es-E(es). (loc(e) = i)  (es-info(es;e)  event-info(ds;da))) 

latex

Definitions

event_system{i:l}, t  T, Id, Type, x. t(x), x:A. B(x), fpf(A; a.B(a)), Knd, top, id-deq, x.A(x), fpf-cap(f; eq; x; z), es-vartype(es; i; x), x:AB(x), es-kind(es; e), Kind-deq, es-valtype(es; e), loc(e), s = t, P  Q, es-E(es), prop{i:l}, decl-state(ds), x:A  B(x), es-val(es; e), es-state(es; i), es-state-when(es; e), <a, b>, b, eq_id(a; b), P  Q, P  Q, P  Q, guard(T), es-info(es;e), event-info(ds;da)

Lemmas

all functionality wrt iff, implies functionality wrt iff, assert wf, eq id wf, subtype rel wf, assert-eq-id, es-state-when wf, subtype rel dep function, subtype rel self, es-val wf, decl-state wf, es-E wf, es-loc wf, es-valtype wf, Kind-deq wf, es-kind wf, es-vartype wf, fpf-cap wf, id-deq wf, top wf, Knd wf, fpf wf, Id wf, event system wf